Add Finite class #2858

kleinreact · 2024-12-30T12:56:16Z

The PR adds the Finite class as well as supplemental instances for most of the standard types.

Finite is a class for types with only finitely many inhabitants and can be considered a more hardware-friendly alternative to Bounded and Enum, utilizing Index instead of Int and vectors instead of lists.

Have a look at the haddock documentation for further insights.

Requires

Linear Clash.Sized.Vector.reverse #2871

Still TODO:

Write a changelog entry (see changelog/README.md)
Check copyright notices are up to date in edited files

martijnbastiaan

Couple of questions! Mostly wondering whether it would make sense to provide an Index-based Enum instead.

martijnbastiaan · 2024-12-30T20:06:27Z

clash-prelude/src/Clash/Explicit/Prelude.hs

+    res  = x :> prev'
+    prev' = case natVal (asNatProxy prev') of
             0 -> repeat def
-             _ -> let next = x +>> prev
-                  in  registerB clk rst en (repeat def) next
+             _ -> let next' = x +>> prev'
+                  in  registerB clk rst en (repeat def) next'


The fact that you have to do this is a pretty strong hint these names shouldn't be in Clash.Prelude. Grepping my projects for prev and next also reveals a number of uses.

That's kind of unavoidable. Every new name we choose might already be picked up in existing user code and I doubt that it's in the interest of the user, if we choose artificially unintuitive names just because of that.

So yes, the user might experience some new warnings about "clashing" names after a Clash update, which are always easy to fix via renaming or hiding the new stuff from Clash.Prelude, in case they are not desired.

Please note that finding a good (and intuitive) naming scheme that doesn't clash with basic existing libraries (in particular base) is a challenge already, especially if the offered primitives are quire fundamental. I also tried to improve the situation here based on some prior experience I had with the finite library, which comes with a similar interface.

I think the point is we write many state machines in Clash and there prev and next are very intuitive local names. Of course you can't avoid all name clashes, but there are some words that are very common in Clash code and prev and next are two examples of that specific category. So I agree with Martijn that trying to come up with an alternative is worthwhile in this specific case.

[edit]
Also, I believe we felt we wanted to move away from primes as a suffix in our code, instead using numeric suffixes to disambiguate. So I believe it'd be better to do that instead of introducing new uses of prime in our code base.
[/edit]

before/after?

prior/later?

back/forward?

Did not think them through much, just throwing it out there.

fpred / fsucc for finite versions of Enum functions?

succ :: a -> a

Successor of a value. For numeric types, succ adds 1.

pred :: a -> a

Predecessor of a value. For numeric types, pred subtracts 1.

I think that if they wanted to enforce that, then they would have added a law. But yeah, those two sentences are kind of misleading indeed.

If the Haddock of a class definition is not normative, what is? They usually use the word law in these cases, but there's no wiggle room in the doc that I see. If they wanted to document something that is common but not normative, I believe they would at the least add the word usually.

[edit]
My point is that these sentences are not misleading. Can you point me to an authoritative text that says otherwise? They are laws. They just didn't use the word law.
[/edit]

[edit 2]
satSucc and satPred are based on Enum. Enum says they should add and subtract one. So the doc for satSucc and satPred says they should add and subtract one.

Originally satSucc and satPred weren't even part of SaturatingNum. But we found that this lead to undesired behaviour of specific instances, so we moved them into the class because they're related enough to justify that.
[/edit 2]

My point is that these sentences are not misleading. Can you point me to an authoritative text that says otherwise? They are laws. They just didn't use the word law.

I'm not aware of any authoritative text, but the style of class requirement descriptions in base and ghc-prim varies a lot, so it doesn't look to me like they have a strict enforcement on wording at this point. I gave some examples below. According to those you need to take the Applicative laws very seriously for example, while the equality laws are more kind of a nice-to-have 🙃.

Eq

The Haskell Report defines no laws for Eq. However, == is customarily expected to implement an equivalence relationship where two values comparing equal are indistinguishable by "public" functions, with a "public" function being one not allowing to see implementation details. For example, for a type representing non-normalised natural numbers modulo 100, a "public" function doesn't make the difference between 1 and 201. It is expected to have the following properties:

Ord

The Haskell Report defines no laws for Ord. However, <= is customarily expected to implement a non-strict partial order and have the following properties:

Applicative

Further, any definition must satisfy the following:

Monad

Instances of Monad should satisfy the following:

satSucc and satPred are based on Enum.

Sure satSucc has a default implementation, which is satSucc s n = satAdd s n 1, but there is no requirement that I cannot chose a different implementation for my own type instances at this point.

It's also a questionable, whether just because of that every class instance should depend on having a Num instance as well. It would be much more user-friendly to have a default signature that requires Num, so the constraint is only required if the user wants to use the default in the first place, e.g.,

satSucc :: SaturationMode -> a -> a -- Default method suitable for types that can represent the number 1 default satSucc :: Num a => SaturationMode -> a -> a satSucc s n = satAdd s n 1 {-# INLINE satSucc #-}

This would elide the requirement on Num for every class instance.

Regarding satSucc and satPred I have primarily not been talking about documentation or implementation, I'm talking about invisible things like design and intent. And also how they changed once we noticed deficiencies.

Sure satSucc has a default implementation, which is satSucc s n = satAdd s n 1, but there is no requirement that I cannot chose a different implementation for my own type instances at this point.

We mean our documentation to be normative. So yes, I definitely interpret it as a requirement that they should add/subtract 1.¹ You yourself argued this above:

Do I miss something fundamental here? I read that like satSucc is equivalent to (+ 1), except for the boundary cases, where the behavior might differ. That's what I consider by "to compatible with each other".

I'd strongly argue that even in the boundary cases the behaviour matches adding/subtracting 1, it's just that (+ 1) does not actually add 1 in those cases.

(continuing with quote from your latest message)

It's also a questionable, whether just because of that every class instance should depend on having a Num instance as well.

I think discussing creating another class for satSucc and satPred is out-of-scope here.

¹ Unless you're talking about boundary cases where the default implementation does not actually satisfy the laws, but then I don't understand why you bring it up.

clash-prelude/src/Clash/Class/Finite/Internal.hs

clash-prelude/src/Clash/Num/Zeroing.hs

clash-prelude/src/Clash/Num/Wrapping.hs

clash-prelude/src/Clash/Num/Saturating.hs

clash-prelude/src/Clash/Class/Finite/Internal.hs

martijnbastiaan · 2025-01-01T20:43:18Z

Another thing to consider: there is at least some overlap with Counter I believe. Perhaps Counter's superclass should be Finite?

kleinreact · 2025-01-02T07:24:22Z

Another thing to consider: there is at least some overlap with Counter I believe. Perhaps Counter's superclass should be Finite?

Good point. Making Finite a superclass would be a recognizable API change tough. Also, you technically can have a Counter instance for a type with infinitely many inhabitants, so adding the superclass requirement here would introduce a limitation.

How about adding another deriving strategy for Counter via FiniteDerive instead, like already present for Enum? Then the users can decide on their own, whether counting via the implicit index order of the Finite instance is exactly what they want.

martijnbastiaan · 2025-01-02T12:08:26Z

Making Finite a superclass would be a recognizable API change tough.

I think however we slice it this PR will be an API change, unless we decide to not export it from Prelude. So that's fine with me (provided that there wouldn't be runtime changes).

How about adding another deriving strategy for Counter via FiniteDerive instead, like already present for Enum? Then the users can decide on their own, whether counting via the implicit index order of the Finite instance is exactly what they want.

I think Finite would count the same as Enum for sum-types right? In that case I don't see the benefit of offering both, but I'm also not opposed to it.

clash-prelude/src/Clash/Class/Finite/Internal.hs

clash-prelude/src/Clash/Class/Finite/Internal/TH.hs

clash-prelude/src/Clash/Class/Finite/Internal/Dictionaries.hs

clash-prelude/src/Clash/Class/Finite/Internal/TH.hs

clash-prelude/src/Clash/Class/Finite/Internal.hs

clash-prelude/tests/Clash/Tests/Laws/Finite.hs

kleinreact · 2025-01-10T19:53:39Z

Could you hide the three internal modules from the Haddock?

👍

[edit]

Also, I think we should have instances for Clash.Sized.Fixed. I don't know if there are any more instances that were overlooked, but that one occurred to me.

I never have used Fixed and don't have much insights into the concept. Maybe we can add that in a later PR.
[/edit]

DigitalBrains1 · 2025-01-10T20:02:35Z

Okay, when this is merged, could you create an issue that we should add the instance?

clash-prelude/src/Clash/Class/Finite/Internal.hs

DigitalBrains1

I had another pass over the Haddock and feel there's still some needed changes.

clash-prelude/src/Clash/Class/Finite.hs

clash-prelude/src/Clash/Class/Finite/Internal.hs

clash-prelude/src/Clash/Class/Finite.hs

clash-prelude/src/Clash/Class/Finite/Internal/Dictionaries.hs

DigitalBrains1

I strongly feel the functions should have been called fpred and fsucc (or finSucc), but since you've made it clear that this is not up for discussion, I suppose I'll yield and approve.

martijnbastiaan

I'm going to neither approve nor deny this PR on the grounds that I strongly feel squatting the names succMaybe in the Prelude is no bueano. The functions Counter exposes could just as well have been called this with slightly different design decisions. They should be called finSucc (in line with satSucc and countSucc) or maybe fsucc.

kleinreact · 2025-02-13T07:54:13Z

The functions Counter exposes could just as well have been called this with slightly different design decisions. They should be called finSucc (in line with satSucc and countSucc) or maybe fsucc.

I propose to switch your point of view, as satSucc and countSucc can have other semantics than succ, while succMaybe is required, by the Enum Compatibility law, to expose the same semantics as Just . succ for all the preimage of succ.

Thus, using the name succMaybe makes this semantic connection explicit, while names like finSucc of fSucc do not. The same applies for pred and predMaybe.

martijnbastiaan · 2025-02-13T08:09:31Z

I don't think I agree with your logic, but more importantly: you are basing your arguments on very subtle details that will be lost on the majority of Clash users. As a result, the API will be less memorable.

kleinreact · 2025-02-13T08:14:35Z

you are basing your arguments on very subtle details

Why do you consider the semantics of a function to be subtle details?

that will be lost on the majority of Clash users. As a result, the API will be less memorable.

How do you know that?

DigitalBrains1 · 2025-02-13T09:11:01Z

Also note that when we add the instance for Fixed, the semantics of the pred and succ of this class will no longer match the semantics of Enum for Fixed.

I really don't feel like participating in this discussion otherwise, but you raise an important point: your laws prohibit compatibility with our existing Enum instance for Fixed. You say both that Finite should enumerate all elements and that it should behave as succ and pred from Enum which don't do that, they add and subtract one.

DigitalBrains1

The laws are contradictory. They state predMaybe and succMaybe should enumerate all values, and simultaneously that they need to be compatible with Enum. Our Fixed type will break this as it can not satisfy both. It is also an example of how they are overconstrained. The Enum compatibility law probably needs to be removed; the existing laws should already fix the behaviour of predMaybe and succMaybe.

kleinreact · 2025-02-13T10:42:19Z

Also note that when we add the instance for Fixed, the semantics of the pred and succ of this class will no longer match the semantics of Enum for Fixed.

It looks to me like the Enum instance for Fixed is wrong then. I consider the successor of 1.5 :: UFixed 2 1 to be 2and not 2.5 according to the Haskell 2010 Language Report.

The current Enum (UFixed 2 1) instance implements a similar behavior as the Enum instance for Float, but the report makes an explicit exception for that particular type. It defines:

For all four numeric types (which are only Int, Integer, Float, and Double) , succ adds 1, and pred subtracts 1.

For any other type the semantics is:

Class Enum deﬁnes operations on sequentially ordered types. The functions succ and pred return the
successor and predecessor, respectively, of a value.

The sequential order of UFixed 2 1 is

0.0, 0.5, 1.0, 1.5, 2.0, 2.5, 3.0, 3.5

and, thus, the successor of 1.5 must be 2.0.

As UFixed 2 1 also has a Bounded instance, there even is proof that the current implementation is wrong, because in that case it is also required that

enumFromThen x y = enumFromThenTo x y bound
  where
    bound | fromEnum y >= fromEnum x = maxBound
          | otherwise = minBound

which does not hold for UFixed 2 1, x = 2.5 and y = 2.0, resulting in

[2.5,2.0,1.5,1.0,0.5,0.0] = []

DigitalBrains1 · 2025-02-13T11:00:52Z

Yeah, we're not going to change Fixed again. Maybe changing it to conform to the class's documentation in the first place was a mistake, but we're not changing it back. We already had the fallout of at least one Clash user losing a lot of time trying to find the regression when we changed it the first time. Plus, being able to get the intuitive behaviour of (+ 1) for degenerate instances of Fixed is also nice.

Also, you're missing the bigger point, it doesn't matter what Fixed does. The Enum laws do not require the type to enumerate each and every element, but your Finite laws do. So somebody out there might already have a type for which they've written an Enum and now want to add a Finite. You can't at the same time fully fix the behaviour by requiring it to enumerate each and every possible value and require it to conform to Enum as well, which does not have that requirement.

Finally, if they really wanted succ and pred to be the successor and predecessor of all possible values a type can take, why didn't they do this for Float and Double? Those also only have a very finite number of inhabitants. A successor and predecessor is completely well-defined for both except for NaN and Inf. Those can be defined just fine as well, it's just less trivial than for a finite number.

[edit]
Why did you re-request a review?
[/edit]

[edit 2]
The other Finite laws state:

Forward Iterate
iterateI (>>= succMaybe) (lowestMaybe @A) = Just <$> (elements @A)
Backward Iterate
iterateI (>>= predMaybe) (highestMaybe @A) = Just <$> reverse (elements @A)

What exactly do you foresee your additional requirement

If a has an Enum instance, it further must satisfy:

Enum Compatibility
succMaybe x = Just y: succ x = y
predMaybe x = Just y: pred x = y

to add? Can you think of an example of a predMaybe or succMaybe that would satisfy the first two laws but need the final law to remove any more ambiguity?
[/edit 2]

kleinreact · 2025-02-13T12:32:26Z

Yeah, we're not going to change Fixed again.

That's not an issue of this PR. It's not conform with Haskell2010 as it is implemented right now. I opened #2888 to keep that separate .

The Enum laws do not require the type to enumerate each and every element, but your Finite laws do.

This is only true for Int, Integer, Float, Double and infinite types. Every finite type that has some sequential order is able to traverse every element according to that order. Otherwise it should not be an instance of Enum in the first place.

You can't at the same time fully fix the behaviour by requiring it to enumerate each and every possible value and require it to conform to Enum as well, which does not have that requirement.

Why not? Every type that doesn't satisfy this requirement simply is not eligible to be an instance of Finite. I don't require anything. I define the class to capture only those types that have that property.

Finally, if they really wanted succ and pred to be the successor and predecessor of all possible values a type can take, why didn't they do this for Float and Double?

Float and Double are infinite types, where all the considerations made by Finite simply don't apply. Sure, on the finite state machines on our desks they are represented by finitely many bits, but on an analog computation architecture, for example, that might not be a limitation.

Why did you re-request a review?

Because you requested changes with the assumption that the laws are contradictory. However, I don't see anything contradicting. If a type cannot satisfy the laws, it simply has no Finite instance.

What exactly do you foresee your additional requirement add?

The user shall be able to expect that succ and succMaybe don't behave contradictory to each other. Hence, any implementation of a Finite instance needs to take this into account.

DigitalBrains1

If a type cannot satisfy the laws, it simply has no Finite instance.

I don't agree and I am way beyond done with all the discussion in this PR.

Unless you remove the Enum compatibility law, I do not want to approve this PR. I'm also still quite conflicted about the naming.

kleinreact · 2025-02-13T19:07:43Z

I don't agree and I am way beyond done with all the discussion in this PR.

Unless you remove the Enum compatibility law, I do not want to approve this PR. I'm also still quite conflicted about the naming.

I understand. The Enum compatibility law is an essential part of the intended design.

Thank you all for the feedback.

kleinreact added enhancement needs-review labels Dec 30, 2024

kleinreact force-pushed the finite-class branch 5 times, most recently from 540afcf to 4d3695c Compare December 30, 2024 18:54

martijnbastiaan reviewed Dec 30, 2024

View reviewed changes

kleinreact force-pushed the finite-class branch 8 times, most recently from 7a1399a to 1130232 Compare January 1, 2025 19:16

kleinreact force-pushed the finite-class branch 2 times, most recently from 9564261 to 80dc978 Compare January 2, 2025 07:17

kleinreact force-pushed the finite-class branch 3 times, most recently from decaec3 to c8821c4 Compare January 7, 2025 07:55

leonschoorl reviewed Jan 7, 2025

View reviewed changes

kleinreact force-pushed the finite-class branch from c8821c4 to 042a148 Compare January 8, 2025 07:26

martijnbastiaan reviewed Jan 8, 2025

View reviewed changes

clash-prelude/tests/Clash/Tests/Laws/Finite.hs Outdated Show resolved Hide resolved

kleinreact force-pushed the finite-class branch 3 times, most recently from cb4795a to 8aeab59 Compare January 10, 2025 08:36

kleinreact force-pushed the finite-class branch from 3719e4a to de1af6f Compare January 11, 2025 02:56

DigitalBrains1 reviewed Jan 13, 2025

View reviewed changes

clash-prelude/src/Clash/Class/Finite/Internal.hs Show resolved Hide resolved

DigitalBrains1 reviewed Jan 13, 2025

View reviewed changes

clash-prelude/src/Clash/Class/Finite/Internal.hs Show resolved Hide resolved

kleinreact force-pushed the finite-class branch 2 times, most recently from e8cf2ec to bbf0415 Compare January 13, 2025 17:25

DigitalBrains1 requested changes Jan 31, 2025

View reviewed changes

kleinreact force-pushed the finite-class branch from bbf0415 to e863bfe Compare February 2, 2025 19:18

kleinreact requested a review from DigitalBrains1 February 2, 2025 19:23

leonschoorl reviewed Feb 3, 2025

View reviewed changes

clash-prelude/src/Clash/Class/Finite/Internal/Dictionaries.hs Outdated Show resolved Hide resolved

kleinreact force-pushed the finite-class branch from e863bfe to d8561b6 Compare February 4, 2025 19:11

kleinreact added 2 commits February 4, 2025 20:22

Add Finite class

6777226

Add tests for Finite laws

8df17ea

kleinreact force-pushed the finite-class branch from d8561b6 to 8df17ea Compare February 4, 2025 19:22

DigitalBrains1 approved these changes Feb 12, 2025

View reviewed changes

martijnbastiaan reviewed Feb 13, 2025

View reviewed changes

DigitalBrains1 requested changes Feb 13, 2025

View reviewed changes

kleinreact requested a review from DigitalBrains1 February 13, 2025 10:42

kleinreact mentioned this pull request Feb 13, 2025

Enum instance of UFixed is not Haskell conform #2888

Open

DigitalBrains1 requested changes Feb 13, 2025

View reviewed changes

kleinreact closed this Feb 13, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add Finite class #2858

Add Finite class #2858

kleinreact commented Dec 30, 2024 •

edited

Loading

martijnbastiaan left a comment

martijnbastiaan Dec 30, 2024

kleinreact Dec 31, 2024

DigitalBrains1 Dec 31, 2024 •

edited

Loading

DigitalBrains1 Dec 31, 2024

gergoerdi Dec 31, 2024

kleinreact Jan 10, 2025

DigitalBrains1 Jan 10, 2025 •

edited

Loading

kleinreact Jan 10, 2025

kleinreact Jan 10, 2025 •

edited

Loading

DigitalBrains1 Jan 10, 2025

martijnbastiaan commented Jan 1, 2025

kleinreact commented Jan 2, 2025

martijnbastiaan commented Jan 2, 2025

kleinreact commented Jan 10, 2025 •

edited

Loading

DigitalBrains1 commented Jan 10, 2025

DigitalBrains1 left a comment

DigitalBrains1 left a comment •

edited

Loading

martijnbastiaan left a comment

kleinreact commented Feb 13, 2025

martijnbastiaan commented Feb 13, 2025

kleinreact commented Feb 13, 2025

DigitalBrains1 commented Feb 13, 2025

DigitalBrains1 left a comment •

edited

Loading

kleinreact commented Feb 13, 2025

DigitalBrains1 commented Feb 13, 2025 •

edited

Loading

kleinreact commented Feb 13, 2025

DigitalBrains1 left a comment

kleinreact commented Feb 13, 2025

Add Finite class #2858

Add Finite class #2858

Conversation

kleinreact commented Dec 30, 2024 • edited Loading

Requires

Still TODO:

martijnbastiaan left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

DigitalBrains1 Dec 31, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

DigitalBrains1 Jan 10, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kleinreact Jan 10, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martijnbastiaan commented Jan 1, 2025

kleinreact commented Jan 2, 2025

martijnbastiaan commented Jan 2, 2025

kleinreact commented Jan 10, 2025 • edited Loading

DigitalBrains1 commented Jan 10, 2025

DigitalBrains1 left a comment

Choose a reason for hiding this comment

DigitalBrains1 left a comment • edited Loading

Choose a reason for hiding this comment

martijnbastiaan left a comment

Choose a reason for hiding this comment

kleinreact commented Feb 13, 2025

martijnbastiaan commented Feb 13, 2025

kleinreact commented Feb 13, 2025

DigitalBrains1 commented Feb 13, 2025

DigitalBrains1 left a comment • edited Loading

Choose a reason for hiding this comment

kleinreact commented Feb 13, 2025

DigitalBrains1 commented Feb 13, 2025 • edited Loading

kleinreact commented Feb 13, 2025

DigitalBrains1 left a comment

Choose a reason for hiding this comment

kleinreact commented Feb 13, 2025

kleinreact commented Dec 30, 2024 •

edited

Loading

DigitalBrains1 Dec 31, 2024 •

edited

Loading

DigitalBrains1 Jan 10, 2025 •

edited

Loading

kleinreact Jan 10, 2025 •

edited

Loading

kleinreact commented Jan 10, 2025 •

edited

Loading

DigitalBrains1 left a comment •

edited

Loading

DigitalBrains1 left a comment •

edited

Loading

DigitalBrains1 commented Feb 13, 2025 •

edited

Loading